An operation check is performed on a control program by using a conventional engineering tool while the engineering tool is connected to the actual control-target device or a simulator. The operation check is generally performed using a technique where, while the control program to be checked is executed, a user monitors and checks the situation of the control program. Further, during the operation check, setting the initial values of the control program and setting parameters during execution are performed by the user entering and setting them.
With the above conventional method, there is a problem in that, in order to execute and check the control program, the user has multiple tasks and therefore the conventional method is time-consuming. Further, with the above method, the user needs to set initial values and parameters during execution beforehand in order to exhaustively check operations, and it takes time to create the initial values and parameters.
In response to the problems with the above conventional method, a device has been proposed that performs the operation check on a control program by using a model checking program (see Patent Literature 1).